As multi-core systems are coming into general use, concurrency-related bugs are a more significant problem for mainstream programmers. The traditional correctness criterion for concurrent programs is the absence of data-races, which occur when two threads access the same shared variable, one of the accesses is a write, and there is no synchronization between them. In general, data-race freedom does not guarantee the absence of concurrency-related bugs. Therefore, different types of errors and correctness criteria have been proposed, such as high-level data races (See reference A listed below), stale-value errors (See references B and C listed below), and several definitions of serializability (or atomicity) (See references D-N listed below). According to these definitions of serializability, a schedule of read and write events performed by a collection of threads is serializable if it is equivalent to a serial schedule, in which each thread's transactions (or atomic sections) are executed in some serial order. These correctness criteria ignore the relationships between shared memory locations, such as invariants and consistency properties, and may not accurately reflect the intentions of the programmer for correct behavior.
Therefore a need exists to overcome the problems with the prior art as discussed above.
The following paragraphs list the references A-N cited above, all of which are incorporated by reference in their entirety. Reference A, C. Artho, K. Havelund, and A. Biere. High-level data races. Journal on Software Testing, Verification and Reliability (STVR), 13(4):207-227, 2003; Reference B and C, respectively, C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In Automated Technology for Verification and Analysis (ATVA'04), number 3299 in LNCS, pages 150-164. Springer, 2004 and M. Burrows and K. R. M. Leino. Finding stale-value errors in concurrent programs. Concurrency and Computation: Practice and Experience, 16(12):1161-1172, 2004;
References D-H, respectively, C. Flanagan and S. Qadeer. A type and effect system for atomicity. In PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 338-349, New York, N.Y., USA, 2003. ACM Press; C. Flanagan and S. Qadeer. Types for atomicity. In TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 1-12, New York, N.Y., USA, 2003. ACM Press; L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proceedings of the Workshop on Runtime Verification (RV'03), 2003. Volume 89(2) of Electronic Notes in Theoretical Computer Science. Elsevier; C. Flanagan and S. N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 256-267, 2004; C. von Praun and T. R. Gross. Atomicity violations in object-oriented programs. Journal of Object Technology, 3(6):103-122, June 2004. Special issue: ECOOP 2003 workshop on FTfJP.
References I-N, respectively, R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In ASE '05: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, pages 233-242, New York, N.Y., USA, 2005. ACM Press; C. Flanagan, S. N. Freund, and M. Lifshin. Type inference for atomicity. In TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 47-58, New York, N.Y., USA, 2005. ACM Press; A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 83-94, New York, N.Y., USA, 2005. ACM Press; S. Lu, J. Tucek, F. Qin, and Y. Zhou. AVIO: Detecting atomicity violations via access interleaving invariants. In Proceedings of the Twelfth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'06), pages 37-48, San Jose, Calif., 2006; and L. Wang and S. D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Transactions on Software Engineering, 32(2):93-110, 2006; L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, (PPoPP'06), pages 137-146, New York, N.Y., 2006